#include <scdl/parser/Symbol.hpp>
#include <scdl/parser/internal.hpp>

#include <cstdlib>
#include <cstring>
#include <iostream>

using std::cout;
using namespace scdl;

class Helper {
        struct Result {
                Symbol **syms;
                Symbol *type, *nextType;
                Result *next;
        } head;

        int elements, currentElement;
        Symbol *substitution[LEVEL_END];

        void link(Result *current, Result *next) {
                next->next = current->next;
                current->next = next;
        }

        Result *unlink(Result *prev, Result *removed) {
                prev->next = removed->next;
                if (removed->syms)
                        delete[] removed->syms;
                delete removed;
                return prev->next;
        }

        Result *dup(Result *current) {
                Result *r = new Result;
                r->syms = new Symbol *[elements];
                memcpy(r->syms, current->syms, elements * sizeof(Symbol *));
                r->type = current->type;
                r->nextType = 0;
                link(current, r);
                return r;
        }

public:
        Helper(int elements)
                : elements(elements)
        {
                head.syms = 0;
                head.next = 0;
        }

        ~Helper()
        {
        }

        bool start(Symbol *sym)
        {
                for (int i = 0; i < LEVEL_END; i++)
                        substitution[i] = 0;

                switch(sym->getCategory()) {
                case CATEGORY_IDENTIFIER_LIST:
                {
                        IdentifierList *list = static_cast<IdentifierList *>(sym);
                        int num = list->getNrElements();
                        Result *current = &head;
                        for (int i = 0; i < num; i++) {
                                Result *next = new Result;
                                next->syms = new Symbol*[elements];
                                next->syms[0] = list->getElement(i);
                                next->nextType = next->syms[0]->getType();
                                link(current, next);
                                current = next;
                        }
                }
                        break;
                case CATEGORY_DEFINITION:
                case CATEGORY_ASSUMPTION:
                case CATEGORY_INTERFACE:
                case CATEGORY_PRODUCT:
                {
                        Result *next = new Result;
                        next->syms = new Symbol*[elements];
                        next->syms[0] = sym;
                        next->nextType = sym->getType();
                        link(&head, next);
                }
                        break;
                default:
                        return false;
                }

                currentElement = 1;
                return true;
        }

        bool next(Symbol *expr)
        {
                Result *prev = &head, *current = prev->next;

                /* First of all, remove non-product values and clear the unused */
                cleanup(false);

                /* Second, check if we have any expectations. */
                Symbol *expected = 0;
                prev = &head, current = prev->next;
                while (current) {
                        Product *p = static_cast<Product *>(current->type);

                        if (!expected)
                                expected = p->leftFactor();
                        else if (!checkType(expected, p->leftFactor(), true)) {
                                expected = 0;
                                break;
                        }

                        prev = current;
                        current = current->next;
                }

                /* Third, try applying. */
                int nrExprs = 1;
                IdentifierList *exprList = 0;
                if (expr->getCategory() == CATEGORY_IDENTIFIER_LIST) {
                        exprList = static_cast<IdentifierList *>(expr);
                        nrExprs = exprList->getNrElements();
                }
                for (int i = 0; i < nrExprs; i++) {
                        Symbol *e;
                        if (exprList)
                                e = exprList->getElement(i);
                        else
                                e = expr;
                        Symbol *exprType = e->getType(expected);
                        if (!exprType)
                                continue;

                        current = head.next;
                        while (current) {
                                Product *p = static_cast<Product *>(current->type);

                                if (checkType(exprType, p->leftFactor(), false)) {
                                        /* Record substitution if any */
                                        if (!checkType(exprType, p->leftFactor(), true)) {
                                                int typeLevel = p->leftFactor()->getTypeLevel();
                                                if (substitution[typeLevel] != 0 &&
                                                    substitution[typeLevel] != exprType)
                                                        goto next;
                                                substitution[typeLevel] = exprType;
#ifdef DEBUG
                                                cout << "substitude ";
                                                p->leftFactor()->prettyPrint(true);
                                                cout << " to ";
                                                exprType->prettyPrint();
                                                cout << "\n";
#endif
                                        }

                                        if (current->nextType)
                                                current = dup(current);
                                        current->syms[currentElement] = e;
                                        Symbol *nextType = p->rightFactor();
                                        if (nextType->getCategory() != CATEGORY_IDENTIFIER_LIST)
                                                current->nextType = nextType;
                                        else {
                                                IdentifierList *list = static_cast<IdentifierList *>(nextType);
                                                int num = list->getNrElements();
                                                current->nextType = list->getElement(0)->getType();
                                                for (int i = 1; i < num; i++) {
                                                        current = dup(current);
                                                        current->nextType = list->getElement(i)->getType();
                                                }
                                        }
                                }
next:
                                current = current->next;
                        }
                }

#ifdef DEBUG
                cout << "Current candidates:\n";
                current = head.next;
                while (current) {
                        cout << "\t";
                        current->nextType->prettyPrint(true);
                        cout << "\n";
                        current = current->next;
                }
#endif

                currentElement ++;
                return (head.next != 0);
        }

        void checkExpected(Symbol *sym)
        {
                /* Keep simple types only at present */
                Result *prev = &head, *current = prev->next;
                while (current) {
                        if(current->type->getCategory() == CATEGORY_PRODUCT) {
                                current = unlink(prev, current);
                                continue;
                        }
                        prev = current;
                        current = current->next;
                }

                if (!sym)
                        return;

                /* Carry out expectation checking */
                prev = &head;
                current = prev->next;
                while (current) {
                        Symbol *substituted = getSubstitution(current->type);
                        if (!checkType(substituted, sym, false)) {
                                current = unlink(prev, current);
                                continue;
                        }

                        prev = current;
                        current = current->next;
                }
        }

        void end()
        {
                cleanup(true);
        }

        void cleanup(bool atEnd)
        {
                Result *prev = &head, *current = prev->next;
                while (current) {
                        current->type = current->nextType;
                        current->nextType = 0;

                        if (current->type == 0 ||
                            ( !atEnd && current->type->getCategory() != CATEGORY_PRODUCT)) {
                                current = unlink(prev, current);
                                continue;
                        }

                        prev = current;
                        current = current->next;
                }
        }

        int getNrResults()
        {
                int n = 0;
                for(Result *i = head.next; i != 0; i = i->next, n++)
                        ;
#ifdef DEBUG
                if (n > 1) {
                        cout << "Multiple types determined.\n";
                        Result *current = head.next;
                        while (current) {
                                cout << "\t";
                                for (int i = 0; i < elements; i++) {
                                        current->syms[i]->prettyPrint();
                                        cout << " ";
                                }
                                cout << "\n";
                                current = current->next;
                        }
                }
#endif
                return n;
        }

        Symbol *getResult(int idx)
        {
                if (idx >= elements)
                        return 0;
                if (!head.next || !head.next->syms)
                        return 0;
                return head.next->syms[idx];
        }

        Symbol *getResultType()
        {
                if (!head.next)
                        return 0;
                return getSubstitution(head.next->type);
        }

        Symbol *getSubstitution(Symbol *sym)
        {
                Symbol *result = sym;
                int typeLevel = result->getTypeLevel();
                if (substitution[typeLevel] != 0)
                        result = substitution[typeLevel];
                return result;
        }
};

Application::Application()
{
}

Application::~Application()
{
}

SymbolCategory Application::getCategory()
{
        return CATEGORY_APPLICATION;
}

void Application::prettyPrint(bool verbose)
{
        cout << "( ";
        for (int i = 0; i < size; i++) {
                elements[i]->prettyPrint();
                cout << " ";
        }
        cout << ")";
}

void Application::determineType(Symbol *expected)
{
        typed = true;

        Helper helper(getNrElements());

        if (!helper.start(getApplier()))
                return;

        int num = getNrArguments();
        for (int i = 0; i < num; i++)
                if (!helper.next(getArgument(i)))
                        return;
        helper.end();
        helper.checkExpected(expected);

        if (helper.getNrResults() != 1)
                return;
        num = getNrElements();
        for (int i = 0; i < num; i++) {
                Symbol *sym = helper.getResult(i);
                if (sym->getCategory() == CATEGORY_DEFINITION)
                        this->updateElement(i, static_cast<Identifier *>(sym)->getDef());
                else
                        this->updateElement(i, sym);
        }
        setType(helper.getResultType());
}

Symbol *Application::getApplier()
{
        if (size)
                return getElement(0);
        return 0;
}

int Application::getNrArguments()
{
        return (getNrElements() - 1);
}

Symbol *Application::getArgument(int idx)
{
        return getElement(idx + 1);
}
